Nuprl Lemma : alle-at1_wf
11,40
postcript
pdf
es
:ES,
i
,
x
:Id,
P
:(vartype(
i
;
x
)
). @
i
always.
P
(
v
)
latex
Definitions
x
:
A
.
B
(
x
)
,
,
t
T
,
@
i
always.
P
(
x
)
,
x
(
s
)
,
x
.
t
(
x
)
Lemmas
alle-at
wf
,
es-when
wf
,
subtype
rel
self
,
es-vartype
wf
,
es-E
wf
,
Id
wf
,
es-loc
wf
,
event
system
wf
origin
es:ES, i, x:Id, P:(vartype(i;x)
). @i always.P(v) 
es:ES, i, x:Id, P:(vartype(i;x)). @i always.P(v) x:A. B(x) T
x. t(x)